Nuprl Definition : inj_mon_hom
13,42
postcript
pdf
InjMonHom(
g
;
h
) == {
f
:MonHom(
g
,
h
)| Inj(|
g
|;|
h
|;
f
)}
latex
Up
groups
1
Wellformedness Lemmas
inj
mon
hom
wf
Definitions
MonHom(
M1
,
M2
)
,
Inj(
A
;
B
;
f
)
,
|
g
|
origin